\begin{tabbing}
$\forall$${\it es}$:ES, $P$:(E$\rightarrow\mathbb{P}$), $R$:(E$\rightarrow$E$\rightarrow\mathbb{P}$).
\\[0ex]single{-}thread{-}generator\{i:l\}(${\it es}$;$P$;$R$)
\\[0ex]$\Rightarrow$ \=(($\forall$$e$, ${\it e'}$:E. $P$($e$) $\Rightarrow$ $P$(${\it e'}$) $\Rightarrow$ ((($e$ $R$\^{}+ ${\it e'}$) $\vee$ ($e$ = ${\it e'}$)) $\vee$ (${\it e'}$ $R$\^{}+ $e$)))\+
\\[0ex]c$\wedge$ ($\forall$$x$, $y$:E. ($P$($x$) \& $P$($y$)) $\Rightarrow$ (($R$\^{}+($x$,$y$)) $\Leftarrow\!\Rightarrow$ ($x$ $<$ $y$)))
\\[0ex]c$\wedge$ ($\forall$$x$, $y$:E. ($R$$\mid$$P$\^{}+($x$,$y$)) $\Leftarrow\!\Rightarrow$ ($R$\^{}+$\mid$$P$($x$,$y$)))
\\[0ex]c$\wedge$ ($\forall$$x$, $y$:E. ($R$$\mid$$P$($x$,$y$)) $\Leftarrow\!\Rightarrow$ ($R$$\mid$$P$\^{}+!($x$,$y$)))
\\[0ex]c$\wedge$ ($\forall$$x$, $y$, ${\it x'}$, ${\it y'}$:E. ($R$$\mid$$P$\^{}+($x$,$y$)) $\Rightarrow$ ($R$$\mid$$P$(${\it y'}$,$y$)) $\Rightarrow$ (($R$$\mid$$P$\^{}+($x$,${\it y'}$)) $\vee$ ($x$ = ${\it y'}$)))
\\[0ex]c$\wedge$ ($\forall$$x$, $y$, ${\it x'}$, ${\it y'}$:E. ($R$$\mid$$P$\^{}+($x$,$y$)) $\Rightarrow$ ($R$$\mid$$P$(${\it x'}$,$x$)) $\Rightarrow$ ($R$$\mid$$P$(${\it y'}$,$y$)) $\Rightarrow$ ($R$$\mid$$P$\^{}+(${\it x'}$,${\it y'}$))))
\-
\end{tabbing}